Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		is_empty(nil)	→ true
2:		is_empty(cons(x,l))	→ false
3:		hd(cons(x,l))	→ x
4:		tl(cons(x,l))	→ cons(x,l)
5:		append(l1,l2)	→ ifappend(l1,l2,is_empty(l1))
6:		ifappend(l1,l2,true)	→ l2
7:		ifappend(l1,l2,false)	→ cons(hd(l1),append(tl(l1),l2))

There are 5 dependency pairs:


8:		APPEND(l1,l2)	→ IFAPPEND(l1,l2,is_empty(l1))
9:		APPEND(l1,l2)	→ IS_EMPTY(l1)
10:		IFAPPEND(l1,l2,false)	→ HD(l1)
11:		IFAPPEND(l1,l2,false)	→ APPEND(tl(l1),l2)
12:		IFAPPEND(l1,l2,false)	→ TL(l1)

The approximated dependency graph contains one SCC: {8,11}.

Consider the SCC {8,11}. The usable rules are {1,2,4}. The constraints could not be solved.

Tyrolean Termination Tool (0.07 seconds) --- May 4, 2006